i, a:Id, T:Type, ds:x:Id fp Type, P:(State(ds)TProp),
init:{f:x:Id fp ds(x)?Top| x:Id. x  dom(ds)  x  dom(f) }.
R-pre-init(i;ds;init;a;T;P)  Realizer 

latex

Definitions	False, P  Q, A, t  T, x:A. B(x), b, , s = t, Prop, Type, x.A(x), x. t(x), f(x), Top, a:A fp B(a), x:AB(x), x:AB(x), P & Q, P  Q, Unit, left+right, f(x)?z, P  Q, @loc x initially v:T, {x:A| B(x) }, (x  l), Realizer, fpf-domain(f), xL.R(x), State(ds), @loc precondition for a(v:T):P State(ds) v, left  right, R-pre-init(i;ds;init;a;T;P), IdDeq, x  dom(f), b, Id
Lemmas	Rplus wf, Rpre wf, decl-state wf, fpf wf, Rall wf, l member wf, fpf-domain wf, Rinit wf, member-fpf-domain, fpf-cap wf, top wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, subtype rel self, fpf-ap wf, Id wf, id-deq wf, bool wf, bnot wf, not wf, assert wf